Termination proof of /tmp/tmpveTMhQ/ExIntrod

Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

primes → sieve(from(s(s(0))))
from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → X
tail(cons(X, Y)) → Y
if(true, X, Y) → X
if(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))
sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

The replacement map contains the following entries:

primes: empty set
sieve: {1}
from: {1}
s: {1}
0: empty set
cons: {1}
head: {1}
tail: {1}
if: {1}
true: empty set
false: empty set
filter: {1, 2}
divides: {1, 2}

↳ CSR

  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

primes → sieve(from(s(s(0))))
from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → X
tail(cons(X, Y)) → Y
if(true, X, Y) → X
if(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))
sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

The replacement map contains the following entries:

primes: empty set
sieve: {1}
from: {1}
s: {1}
0: empty set
cons: {1}
head: {1}
tail: {1}
if: {1}
true: empty set
false: empty set
filter: {1, 2}
divides: {1, 2}

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

primes → sieve(from(s(s(0))))
from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → X
tail(cons(X, Y)) → Y
if(true, X, Y) → X
if(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))
sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

The replacement map contains the following entries:

primes: empty set
sieve: {1}
from: {1}
s: {1}
0: empty set
cons: {1}
head: {1}
tail: {1}
if: {1}
true: empty set
false: empty set
filter: {1, 2}
divides: {1, 2}

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {sieve, from, s, head, tail, filter, divides, SIEVE, FROM, FILTER, TAIL} are replacing on all positions.
For all symbols f in {cons, if, IF} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

PRIMES → SIEVE(from(s(s(0))))
PRIMES → FROM(s(s(0)))
FILTER(s(s(X)), cons(Y, Z)) → IF(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))

The collapsing dependency pairs are DP_c:

TAIL(cons(X, Y)) → Y
IF(true, X, Y) → X
IF(false, X, Y) → Y

The hidden terms of R are:

from(s(X))
filter(s(s(X)), Z)
filter(X, sieve(Y))
sieve(Y)

Every hiding context is built from:

s on positions {1}
from on positions {1}
filter on positions {1, 2}
sieve on positions {1}
cons on positions {1}

Hence, the new unhiding pairs DP_u are :

TAIL(cons(X, Y)) → U(Y)
IF(true, X, Y) → U(X)
IF(false, X, Y) → U(Y)
U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
U(filter(x_0, x_1)) → U(x_0)
U(filter(x_0, x_1)) → U(x_1)
U(sieve(x_0)) → U(x_0)
U(cons(x_0, x_1)) → U(x_0)
U(from(s(X))) → FROM(s(X))
U(filter(s(s(X)), Z)) → FILTER(s(s(X)), Z)
U(filter(X, sieve(Y))) → FILTER(X, sieve(Y))
U(sieve(Y)) → SIEVE(Y)

The TRS R consists of the following rules:

primes → sieve(from(s(s(0))))
from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → X
tail(cons(X, Y)) → Y
if(true, X, Y) → X
if(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))
sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

The set Q consists of the following terms:

primes
from(x0)
head(cons(x0, x1))
tail(cons(x0, x1))
if(true, x0, x1)
if(false, x0, x1)
filter(s(s(x0)), cons(x1, x2))
sieve(cons(x0, x1))

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 8 less nodes.
The rules FILTER(s(s(z0)), cons(z1, z2)) → IF(divides(s(s(z0)), z1), filter(s(s(z0)), z2), cons(z1, filter(z0, sieve(z1)))) and IF(true, x0, x1) → U(x0) form no chain, because ECap^µ(IF(divides(s(s(z0)), z1), filter(s(s(z0)), z2), cons(z1, filter(z0, sieve(z1))))) = IF(divides(s(s(z0)), z1), filter(s(s(z0)), z2), cons(z1, filter(z0, sieve(z1)))) does not unify with IF(true, x0, x1). The rules FILTER(s(s(z0)), cons(z1, z2)) → IF(divides(s(s(z0)), z1), filter(s(s(z0)), z2), cons(z1, filter(z0, sieve(z1)))) and IF(false, x0, x1) → U(x1) form no chain, because ECap^µ(IF(divides(s(s(z0)), z1), filter(s(s(z0)), z2), cons(z1, filter(z0, sieve(z1))))) = IF(divides(s(s(z0)), z1), filter(s(s(z0)), z2), cons(z1, filter(z0, sieve(z1)))) does not unify with IF(false, x0, x1).

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ QCSDP

              ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {sieve, from, s, head, tail, filter, divides} are replacing on all positions.
For all symbols f in {cons, if} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
U(filter(x_0, x_1)) → U(x_0)
U(filter(x_0, x_1)) → U(x_1)
U(sieve(x_0)) → U(x_0)
U(cons(x_0, x_1)) → U(x_0)

The TRS R consists of the following rules:

primes → sieve(from(s(s(0))))
from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → X
tail(cons(X, Y)) → Y
if(true, X, Y) → X
if(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))
sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

The set Q consists of the following terms:

primes
from(x0)
head(cons(x0, x1))
tail(cons(x0, x1))
if(true, x0, x1)
if(false, x0, x1)
filter(s(s(x0)), cons(x1, x2))
sieve(cons(x0, x1))

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

U(s(x_0)) → U(x_0)
U(from(x_0)) → U(x_0)
U(filter(x_0, x_1)) → U(x_0)
U(filter(x_0, x_1)) → U(x_1)
U(sieve(x_0)) → U(x_0)
U(cons(x_0, x_1)) → U(x_0)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ QCSDP

              ↳ QCSDPSubtermProof

                ↳ QCSDP

                  ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {sieve, from, s, head, tail, filter, divides} are replacing on all positions.
For all symbols f in {cons, if} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

primes → sieve(from(s(s(0))))
from(X) → cons(X, from(s(X)))
head(cons(X, Y)) → X
tail(cons(X, Y)) → Y
if(true, X, Y) → X
if(false, X, Y) → Y
filter(s(s(X)), cons(Y, Z)) → if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))
sieve(cons(X, Y)) → cons(X, filter(X, sieve(Y)))

The set Q consists of the following terms:

primes
from(x0)
head(cons(x0, x1))
tail(cons(x0, x1))
if(true, x0, x1)
if(false, x0, x1)
filter(s(s(x0)), cons(x1, x2))
sieve(cons(x0, x1))

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.